$\forall$$T$:Type\{i\}. ma{-}interface\{i:l\}($T$) $\in$ Type\{i'\}